\begin{tabbing}
$\forall$\=${\it es}$:ES, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$), $f$:(E(${\it Ia}$)$\rightarrow$$B$), $Q_{1}$,\+
\\[0ex]$Q_{2}$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $g$:(E(${\it Ib}$)$\rightarrow$E).
\-\\[0ex]$Q_{1}$ $\Leftarrow\!\Rightarrow$ $Q_{2}$ $\Rightarrow$ ($g$ glues ${\it Ia}$:$Q_{1}$ $--$$f$$\rightarrow$ ${\it Ib}$:$R$ $\Leftarrow\!\Rightarrow$ $g$ glues ${\it Ia}$:$Q_{2}$ $--$$f$$\rightarrow$ ${\it Ib}$:$R$)
\end{tabbing}